Inference at * 
Iof proof for Lemma bimplies transitivity:


  u,v,w:. ((u  v))  ((v  w))  ((u  w)) 

latex

 by InteriorProof ((((((RepeatMFor 3 (D 0)) 
CollapseTHENM (BoolEval))) 
CollapseTHENM (
CollapseTHENM (AbReduce 0))) 
CollapseTHEN ((Auto_aux (first_nat 1:n) ((first_nat 1:n
CollapseTHEN ((Aut),(first_nat 3:n)) (first_tok :t) inil_term))) 

latex

C.

Definitions	ff, t  T, True, if b then t else f fi , tt, b, P  Q, False,
Lemmas	bool wf, false wf, true wf